Introduction to Higher-Order Categorical Logic
Joachim Lambek
、
P.J. Scott
ここ
で出てきた
これ
や
『圏論の歩き方』
など、
型付きラムダ計算とCCCと直観主義論理
の関係を調べると頻繁に参照されている